I tried to unload the plugin and it had no effect.
it would be nice if it switched back to the jedit default look and feel (although
it would be a bad idea to try to do that while jedit is exiting - only when the plugin
is unloaded due to user request).
| Submitted | ezust - 2008-03-25 - 02:55:50z | Assigned | nobody |
|---|---|---|---|
| Priority | 5 | Category | None |
| Status | Open | Group | None |
| Resolution | None | Visibility | No |